es:event_system{i:l}, L:(Id List).
fischer{x:ut2, try:ut2, taken:ut2, contending:ut2, free:ut2, mine:ut2, wanted:ut2, z:ut2}
fischer(es; L)
 (e:es-E(es). f-event{x:ut2}(es; L; e)  prop{i:l}) 

latex

Definitions	False, A  B, x:A. B(x), mkid{$x:ut2}, A, (x  l), A c B, f-event{$x:ut2}(es; L; e), prop{i:l}, t  T, P  Q, Id, x:A. B(x), b, P  Q, l_all(L; T; x.P(x)), @e(xv), P  Q, es-dtype(es; i; x; T), , fischer
Lemmas	event system wf, Id wf, fischer wf, es-E wf, es-when wf, es-after wf, not wf, select wf, length wf1, nat wf